COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE PREDCONST SEXP 1[R<==350] DECLARE PREDCONST LIST 1[R<==350]
C00005 ENDMK
C⊗;
DECLARE PREDCONST SEXP 1[R<==350]; DECLARE PREDCONST LIST 1[R<==350];

	DECLARE INDVAR X X0 X1 X2 Y Y0 Y1 Y2 Z Z0 Z1 Z2; DECLARE INDVAR x
x0 x1 x2 y y0 y1 y2 z z0 z1 z2 eps SEXP; DECLARE INDVAR u u0 u1 u2 v v0 v1
v2 w w0 w1 w2 eps LIST; DECLARE INDCONST NILL eps LIST;

	AXIOM SEXP: ALL x.SEXP x;; AXIOM LIST: ALL u.LIST u;;

	MOREGENERAL SEXP >= {LIST};

	DECLARE OPCONST CONS 2; DECLARE OPCONST CAR 1[R <== 600]; DECLARE
OPCONST CDR 1[R <== 600];

	DECLARE PREDCONST ATOM 1[R <== 500]; DECLARE PREDCONST NULL 1[R
<== 500];

	AXIOM CONS:
	ALL x y.SEXP CONS(x,y)
	ALL x u.LIST CONS(x,u) ;;

	AXIOM CAR:
	ALL x.(not ATOM x implies SEXP CAR x) ;;

	AXIOM CDR:
	ALL x.(not ATOM x implies SEXP CDR x)
	ALL u.(not u=NILL implies LIST CDR u) ;;

	AXIOM NILL:
	ALL u.(ATOM u iff u = NILL)
	ALL u.(NULL u iff u = NILL) ;;

	AXIOM LISP:
	ALL x y.not ATOM CONS(x,y)
	ALL x y.(CAR CONS(x,y) = x)
	ALL x y.(CDR CONS(x,y) = y)
	ALL y.(not ATOM y implies y = CONS(CAR y,CDR y)) ;;

	DECLARE PREDCONST IN(SEXP,SEXP)[L<==250,R<==255];

	AXIOM IN:
	ALL x.(not ATOM x implies CAR x IN x)
	ALL x.(not ATOM x implies CDR x IN x)
	ALL x y.(x IN CONS(x,y))
	ALL x y.(y IN CONS(x,y))
	ALL x.not x IN x
	ALL x y z.(x IN y and y IN z implies x IN z) ;;

	DECLARE PREDPAR P 1;

	AXIOM INDUCTION:
	ALL x.(ATOM x implies P(x)) and ALL x.(not ATOM x and P(CAR x) and
P(CDR x) implies P(x)) implies ALL x.P(x)
	P(NILL) and ALL u.(not (u=NILL) and P(CDR u) implies P(u)) implies
ALL u.P(u)
	ALL x.(ATOM x implies P(x)) and ALL x.(ALL y.(y IN x implies
P(y))) implies ALL x.P(x) ;;